agree_on_common(T;as;bs)
== Case of as
== Canil  True
== Caa.as', rec:  Case of bs
== Caa.as', rec:  Canil  True
== Caa.as', rec:  Cab.bs', rec:  (a  bs) & agree_on_common(T;as';bs)
== Caa.as', rec:  Cab.bs', rec:   (b  as) & agree_on_common(T;as;bs')
== Caa.as', rec:  Cab.bs', rec:   a = b & agree_on_common(T;as';bs')
(recursive) 

latex

---

clarification:

agree_on_common(T;as;bs)
== Case of as
== Canil  True
== Caa.as', rec:  Case of bs
== Caa.as', rec:  Canil  True
== Caa.as', rec:  Cab.bs', rec:  (a  bs  T) & agree_on_common(T;as';bs)
== Caa.as', rec:  Cab.bs', rec:   (b  as  T) & agree_on_common(T;as;bs')
== Caa.as', rec:  Cab.bs', rec:   a = b  T & agree_on_common(T;as';bs')
(recursive) 

latex

Definitions	Y, True, P  Q, A, (x  l), P & Q
FDL editor aliases	agree_on_common